Nuprl Lemma : member_wf
11,40
postcript
pdf
A
:Type,
a
:
A
. (
a
A
)
Type
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
origin
A:Type, a:A. (a 
A) Type A:Type, a:A. (a A) Type Tx:A. B(x)